Back التحقق الشكلي Arabic Formální verifikace Czech Τυπική επαλήθευση Greek Formal verification English Verificación formal Spanish درستییابی صوری Persian Vérification formelle French אימות תוכנה HE Verifica formale Italian 形式的検証 Japanese
Egiaztapen formala (hardware eta softwareen sistemei dagokionez), algoritmo jakin bat espezifikazio formal batekiko zuzena dela frogatzean datza, horretarako matematikak eskaintzen dituen metodo formalak medio direlarik.[1]
Algoritmo hauen egiaztapena gauzatzako, dagokion sistemaren (hardware edo softwarea, kasuak kasu) eredu matematiko abstraktu batean oinarritzen den froga formal bat eman behar da. Hauek dira sistemen eredutzat erabiltzen diren eredu matematiko batzuk: egoera makina finituak, etiketadun igarotze sistemak, Petriren sareak, bektore batuketarako sistemak, automata denborizatuak, automata hibridoak, prozesuen aljebra, semantika operazionala eta Hoareren logika.[2]